\begin{tabbing}
ma{-}single{-}effect1($x$;$A$;$y$;$B$;$k$;$T$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=with declarations \+
\\[0ex]ds:fpf{-}join(IdDeq;$x$ : $A$;$y$ : $B$)
\\[0ex]da:$k$ : $T$
\\[0ex]effect of $k$(v) is $x$ := $\lambda$$s$,$v$. $f$($s$($x$),$s$($y$),$v$) s v
\-
\end{tabbing}